COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	
C00008 ENDMK
C⊗;

ACCOMPLISHMENTS IN FORMAL REASONING


1. Christopher Goad,  a student research assistant, has  succeeded in
modifying  McCarthy's knowledge formalism so  that conclusions to the
effect that an individual does not  know something can be drawn.   In
all previous  knowledge formalisms,  this has  been possible  only in
trivial cases,  and it is fundamental in making machines reason about
knowledge, because they have to know when their  present knowledge is
insufficient to answer a question so they can search for more.

2. John  McCarthy has identified  a class of  problems called Boolean
search problems that admit very fast parallel solution algorithms and
has shown how many of the quasi-static problems encountered in AI can
be transformed into Boolean search form.

3.   Zohar Manna  has shown how  recursive programs  often admit more
defined  fixed  points  than  the  minimal  fixed  points  that  have
previously been studied.   He calls them optimal fixed  point and has
determined many of their properties.

4. The  algorithm for proving sentences in monadic predicate calculus
has been debugged and has been incorporated into FOL.

5. Many user oriented improvements to the FOL program  have been made
during this period.  They include several new quantifier manipulation
commands, new printing routines,  machine language changes  effecting
overall  efficiency, updated  versions of  the  tautology and  tauteq
routines.  In addition  CMU has requested a version of FOL and we are
bringing it up there.  This  work is being done by Richard  Weyhrauch
and Bill Glassmire.

6.  Zohar Manna  has explored  the  applicability of  a technique  of
"intermittent assertions" due to Burstall for verifying programs, has
compared it with  other techniques on a  number of problems, and  has
demonstrated that it is potentially the most practical technique.


GOALS FOR JULY TO OCTOBER 1976

1.    A  formalism for  describing  sources  of  information will  be
developed and checked by writing  a program that will find  telephone
numbers form the telephone  number files at a number  of computers on
the  ARPA net.   No changes in  the existing files  will be required.
This will be a  step towards making the  computer files all over  the
country accessible  in a uniform  way without requiring that  they be
redesigned.

2.   Pattern  matching has  mostly involved  matching a pattern  to a
symbolic expression.  Dave Wilkins is working on matching patterns to
non-symbolic situations, e.g. situations in the real world.

3.  The McCarthy-Painter  compiler  will be  proved  correct in  FOL.
(This has taken longer than was expected).

4.  A good way of filing already proved theorems for future use  will
be implemented in FOL.

5.  There are  several projects for building needed  features of FOL.
They include: the ability  to handle more than one proof at a time, a
facility for  stating and  checking  goals and  subgoals, and  a  new
version of the FOL machinery for using direct observation of the real
world in making deductions

6.   Zohar   Manna  will   investigate  applying   the  "intermittent
assertions" technique to the automatic synthesis  of programs meeting
given  specifications.   He is  also investigating  the class  of all
fixed  points  of  recursive  programs  and  looking  for   practical
applications of his optimal fixed point approach.